ePMC

Benchmark

Model:	firewire v.2 (MDP)
Parameter(s)	explicit_timer = False, delay = 3, deadline = 200
Property:	time_max (exp-reward)

Invocation (default)

java -Xms10240m -Xmx10240m -jar ../epmc-standard.jar check --model-input-files firewire.false.jani --model-input-type jani --property-input-names time_max --translate-messages false --value-floating-point-output-native true --graphsolver-iterative-stop-criterion relative --graphsolver-iterative-tolerance 1e-6 --const delay=3,deadline=200

Execution

Walltime:	1.2609846591949463s
Return code:	0
Relative Error:	6.02372666506689e-05

Log

assertions-disabled
model-checking
analysing-property time_max
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-done 4093 0
iterating
iterating-done 1940 0
num-states-in-filter 1 "initial"
printing-all-filter-results
print-filter 0 0 298.98198905727145
model-checking-done 0
command-check-result-is 298.98198905727145 time_max